%% Author: Francis Stephens
%% Created: 8 Jan 2008
%% Description: TODO: Add description to davis_putnam
-module(no_cp_most_common_first_dp).

%%
%% Include files
%%

-include("sat_records.hrl").
-include("sat_macros.hrl").

%%
%% Exported Functions
%%
-export([get_functions/0]).

-compile(export_all).

%%
%% API Functions
%%

%%
%% Local Functions
%%

%%
%%	Returns the function which define a Davis-Putnam SAT solver as a #dp_funs.
%%
get_functions() ->
	Pre_Funs = [fun sat_algorithms:is_formula_satisfiable/1],
    Branch_Fun = fun most_common_first:branch_fun/1,
	Post_Funs = [],
	Init_Sat_State = fun sat_algorithms:null_metadata/1,
	#dp_funs{strategy_name=no_cp_most_common_first_dp,pre_funs=Pre_Funs,branch_fun=Branch_Fun,post_funs=Post_Funs,init_sat_state=Init_Sat_State}.